A, B:msga{i:l}. ma-frame-compat(A;B)  Prop{i'} 

latex

Definitions

t  T, Valtype(da;k), State(ds), IdLnk, Knd, x:AB(x), Void, Type, x.A(x), x:A. B(x), x. t(x), 2of(t), rcv(l,tg), KindDeq, f(x)?z, type List, 1of(t), x:AB(x), Id, Top, a:A fp B(a), ||as||, P  Q, False, A, P & Q, AB, i  j < k, , {x:A| B(x) }, {i..j}, b, a<b, #$n, IdDeq, Prop, locl(a), IdLnkDeq, product-deq(A;B;a;b), x  dom(f), l[i], f(a), s = t, deq-member(eq;x;L), left+right, P  Q, x,y. t(x;y), xdom(f). v=f(x)   P(x;v), z != f(x)  P(a;z), <a,b>, map(f;as), (x  l), P  Q, MsgA, M.ds(x), M.dout(l,tg), (s1  s2 mod x), M.da(a), M.state, M.rframe(A.sends tfL of k on l), M.bframe(k sends on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B)

Lemmas

msga wf, iff wf, l member wf, map wf, fpf-val wf, fpf-all wf, deq-member wf, not wf, top wf, int seg wf, select wf, assert wf, fpf-dom wf, product-deq wf, idlnk-deq wf, locl wf, id-deq wf, length wf1, fpf-trivial-subtype-top, Id wf, ma-state wf, ma-valtype wf, pi1 wf, fpf-cap wf, Kind-deq wf, rcv wf, pi2 wf, Knd wf, IdLnk wf